Nuprl Lemma : w-null_wf
11,40
postcript
pdf
T
,
TA
:(Id
Type),
M
:(IdLnk
Id
Type). NullMachine
w-automaton(
T
;
TA
;
M
)
latex
Definitions
w-automaton(
T
;
TA
;
M
)
,
NullMachine
,
inr
x
,
,
,
<
a
,
b
>
,
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
Knd
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
x
.
A
(
x
)
,
[]
,
type
List
,
x
:
A
B
(
x
)
,
f
(
a
)
,
IdLnk
,
x
:
A
B
(
x
)
,
Id
,
t
T
,
Type
Lemmas
Id
wf
,
IdLnk
wf
,
Knd
wf
,
kindcase
wf
,
rationals
wf
,
nat
wf
,
it
wf
origin
T, TA:(Id
Type), M:(IdLnkIdType). NullMachine 
w-automaton(T;TA;M) T, TA:(IdType), M:(IdLnkIdType). NullMachine w-automaton(T;TA;M) 
x. t(x)x:A. B(x)x,y. t(x;y)x.A(x)
B(x)B(x) T